\usepackage{relsize}
\usepackage{amsmath}
\usepackage{url}

\usepackage{listings}

%\usepackage{color}
%
%\definecolor{Brown}{cmyk}{0,0.49,0.71,0.37}
%\definecolor{RoyalBlue}{cmyk}{0.71,0.53,0,0.12}
%\definecolor{OliveGreen}{cmyk}{0.64,0,0.95,0.40}
%\definecolor{Red}{cmyk}{0,0.80,0.80,0.10}
%\definecolor{Gray}{cmyk}{0.2,0.2,0.2,0.2}
%\definecolor{Black}{cmyk}{0,0,0,1}
\lstdefinelanguage{X10}%
  {morekeywords={abstract,break,case,catch,class,%
      const,continue,default,do,else,extends,false,final,%
      finally,for,goto,if,implements,import,instanceof,%
      interface,label,native,new,null,package,private,protected,%
      public,return,static,super,switch,synchronized,this,throw,%
      throws,transient,true,try,volatile,while,%
      async,atomic,when,foreach,ateach,finish,clocked,%
      type,here,%
      self,property,%
      proto,assert,%
      future,to,has,as,var,val,def,where,in,%
      value,or,await,current,any},%
   basicstyle=\normalfont\ttfamily,%\color{Red},%
   keywordstyle=\bf\ttfamily,%\color{OliveGreen},%
   commentstyle=\normalfont\ttfamily,%\color{Gray},%
   identifierstyle=\normalfont\ttfamily,%\color{Red},%
   stringstyle=\normalfont\ttfamily,%
   tabsize=4,%
   showstringspaces=false,%
   sensitive,%
   morecomment=[l]//,%
   morecomment=[s]{/*}{*/},%
   morestring=[b]",%
   morestring=[b]',%
   columns=fullflexible,%
   mathescape=false,%
   keepspaces=true,%
   showlines=false,%
   breaklines=true,%
   breakatwhitespace=true,%
   postbreak={},%
   %breakautoindent=true,%
   %breakindent=0pt,%
   %prebreak={},%
  }

\lstnewenvironment{xtenmath}
  {\lstset{language=X10,breaklines=false,captionpos=b,xleftmargin=2em,mathescape=true}}
  {}

\lstnewenvironment{xten}
  {\lstset{language=X10,breaklines=false,captionpos=b}} %,xleftmargin=2em
  {}

%{numbers=left, numberstyle=\tiny, stepnumber=2, numbersep=5pt
% numbers=left,
\lstset{language=x10,basicstyle=\ttfamily\small}
%\lstset{language=java,basicstyle=\ttfamily\small}


\usepackage[ruled]{algorithm} % [plain]
\usepackage[noend]{algorithmic} % [noend]
\renewcommand\algorithmiccomment[1]{// \textit{#1}} %


% For fancy end of line formatting.
\usepackage{microtype}


% For smaller font.
\usepackage{pslatex}


\usepackage{xspace}
\usepackage{yglabels}
\usepackage{yglang}
\usepackage{ygequation}
%\usepackage{graphicx}
%\usepackage{epstopdf}

\newcommand{\formalrule}[1]{\mbox{\textsc{\scriptsize #1}}}
\newcommand{\myrule}[2]{\textbf{Rule #1:} #2.}
%\newcommand{\myrule}[1]{\textsc{\codesmaller #1 Rule}}
\newcommand{\umyrule}[1]{\textbf{\underline{\textsc{\codesmaller #1 Rule}}}}


% \small \footnotesize \scriptsize \tiny
% \codesize and \scriptsize seem to do the same thing.
% \newcommand{\code}[1]{\texttt{\textup{\footnotesize #1}}}
% \newcommand{\code}[1]{\texttt{\textup{\codesize #1}}}
\newcommand{\normalcode}[1]{\texttt{\textup{#1}}}
\def\codesmaller{\small}
\newcommand{\myCOMMENT}[1]{\COMMENT{\small #1}}
\newcommand{\code}[1]{\texttt{\textup{\codesmaller #1}}}
% \newcommand{\code}[1]{\ifmmode{\mbox{\smaller\ttfamily{#1}}}
%                       \else{\smaller\ttfamily #1}\fi}
\newcommand{\smallcode}[1]{\texttt{\textup{\scriptsize #1}}}

% See: \usepackage{bold-extra} if you want to do \textbf
\newcommand{\keyword}[1]{\code{#1}}

% For new, method invocation, and cast:
\newcommand{\hparen}[1]{\code{(}#1\code{)}}

\newcommand{\hgn}[1]{\lt#1\gt} % type parameters and generic method parameters

\newcommand{\Own}{{\it O}}
\newcommand{\Ifn}[1]{\ensuremath{I(#1)}}
\newcommand{\Ofn}[1]{\ensuremath{O(#1)}}
\newcommand{\Cooker}[1]{\ensuremath{{\kappa}(#1)}}
\newcommand{\Owner}[1]{\ensuremath{{\theta}(#1)}}
\newcommand{\Oprec}[0]{\ensuremath{\preceq_{\theta}}}
\newcommand{\Tprec}[0]{\ensuremath{\preceq^T}}
\newcommand{\TprecNotEqual}[0]{\ensuremath{\prec^T}}
\newcommand{\OprecNotEqual}[0]{\ensuremath{\prec_{\theta}}}
\newcommand{\IfnDelta}[1]{\ensuremath{I_\Delta(#1)}}
\newcommand\Abs[1]{\ensuremath{\left\lvert#1\right\rvert}}
\newcommand{\erase}[1]{\ensuremath{\Abs{#1}}}

\newcommand{\CookerH}[1]{\ensuremath{{\kappa}_H(#1)}}
\newcommand{\IfnH}[1]{\ensuremath{I_H(#1)}}
\newcommand{\OwnerH}[1]{\ensuremath{{\theta}_H(#1)}}
\newcommand{\Gdash}[0]{\ensuremath{\Gamma \vdash }}
\newcommand{\reducesto}[0]{\rightsquigarrow}
\newcommand{\reduce}[0]{\rightsquigarrow}


%% For typesetting theorems and some math symbols (\rightsquigarrow).
\usepackage{amssymb}
% \usepackage{amsthm}  definition of proof already exists

\usepackage{color}
\definecolor{light}{gray}{.75}


\newcommand{\todo}[1]{\textbf{[[#1]]}}
%% To disable, just uncomment this line:
%\renewcommand{\todo}[1]{\relax}

%% Additional todo commands:
\newcommand{\TODO}[1]{\todo{TODO: #1}}

\newcommand\xX[1]{$\textsuperscript{\textit{\text{#1}}}$}


\newcommand{\ol}[1]{\overline{#1}}
\newcommand{\nounderline}[1]{{#1}}


%% Commands used to typeset the FIGJ type system.
\newcommand{\typerule}[2]{
\begin{array}{c}
  #1 \\
\hline
  #2
\end{array}}


%% Commands used to typeset the FOIGJ type system.
\newcommand{\inside}{\prec}
\newcommand{\visible}{{\it visible}}
\newcommand{\placeholderowners}{{\it placeholderowners}}
\newcommand{\nullexpression}{{\tt null}}
\newcommand{\errorexpression}{{\tt error}}
\newcommand{\locations}{{\it locations}} %% \mathop{\mathit{locations}}}
\newcommand{\xo}{{\tt X^O}}
\newcommand{\no}{{\tt N^O}}
\newcommand{\co}{{\tt C^O}}
\newcommand{\I}{\it I}


\newcommand\mynewcommand[2]{\newcommand{#1}{#2\xspace}}

\mynewcommand{\hA}{\code{A}} % inVariant definition
\mynewcommand{\hB}{\code{B}} % inVariant definition

\mynewcommand{\hI}{\code{I}} % iparam

% In the syntax: \hI or ReadOnly or Mutable or Immut
\mynewcommand{\hJ}{\code{J}}
\mynewcommand{\hO}{\code{O}}
\mynewcommand{\ho}{\code{o}}
\mynewcommand{\hnull}{\code{null}}
\mynewcommand{\htrue}{\code{true}}
\mynewcommand{\hfalse}{\code{false}}

\mynewcommand{\hX}{\code{X}} % vars
\mynewcommand{\hY}{\code{Y}} % vars
\mynewcommand{\hC}{\code{C}} % class
\mynewcommand{\hD}{\code{D}} % class
\mynewcommand{\hc}{\code{c}} % cooker
\mynewcommand{\hp}{\code{p}} % cooker
\mynewcommand{\hL}{\code{L}} % class decl
\mynewcommand{\hM}{\code{M}} % Method decl
\mynewcommand{\hN}{\code{N}} % Non-variable type
\mynewcommand{\hm}{\code{m}} % method
\mynewcommand{\he}{\code{e}} % expression
\mynewcommand{\hg}{\code{g}}
\mynewcommand{\hv}{\code{v}} % value
\mynewcommand{\hl}{\code{l}} % location in the store
\mynewcommand{\lroot}{\code{l}_\top} % root
\mynewcommand{\lthis}{\code{l}_\smallcode{this}} % this
\mynewcommand{\hx}{\code{x}} % method parameter
\mynewcommand{\hz}{\code{z}} % method parameter
\mynewcommand{\hq}{\code{q}}
\mynewcommand{\hf}{\code{f}} % field
\mynewcommand{\hy}{\code{y}} % field
\mynewcommand{\hF}{\code{F}} % field declaration
\mynewcommand{\hT}{\code{T}} % types (vars or non vars)
\mynewcommand{\hU}{\code{U}} % types (vars or non vars)
\mynewcommand{\hV}{\code{V}} % closed types
\mynewcommand{\hS}{\code{S}}
\mynewcommand{\hsub}{\code{/}} % substitute (reduction rules)

\mynewcommand{\unknown}{\code{?}}
\mynewcommand{\hand}{\code{~and~}}
\mynewcommand{\hor}{\code{~or~}}
\mynewcommand{\hthis}{\code{this}} % this
\mynewcommand{\hclass}{\code{class}}
\mynewcommand{\hreturn}{\code{return}}
\mynewcommand{\hhnew}{\code{new}}
\newcommand{\initsep}[0]{;} % tried \| and \dagger
\newcommand{\initsets}[2]{\lb#1\initsep#2\rb}
\newcommand{\myinit}[2]{\S{}\lb#1\initsep#2\rb}
\mynewcommand{\mycooked}{\S{}\lb\initsep\rb}
\newcommand{\hnew}[1]{\code{new}~#1}
\newcommand{\hval}[3]{\code{val}~#1~=~#2;#3}

\newcommand{\lt}{\code{<}}%{\mathop{\textrm{\tt <}}}
\newcommand{\gt}{\code{>}}%{\mathop{\textrm{\tt >}}}

\mynewcommand{\this}{\keyword{this}}
\mynewcommand{\Object}{\code{Object}}
\mynewcommand{\const}{\keyword{const}} %C++ keyword
\mynewcommand{\mutable}{\keyword{mutable}} %C++ keyword
\mynewcommand{\romaybe}{\keyword{romaybe}} %Javari keyword

%% Define the behaviour of the theorem package.
%% Use http://math.ucsd.edu/~jeggers/latex/amsthdoc.pdf for reference.

%\newtheorem{theorem}{Theorem}[section]
%\newtheorem{definition}[theorem]{Definition}
%\newtheorem{lemma}[theorem]{Lemma}
%\newtheorem{corollary}[theorem]{Corollary}
%\newtheorem{fact}[theorem]{Fact}
%\newtheorem{example}[theorem]{Example}
%\newtheorem{remark}[theorem]{Remark}


\mynewcommand{\IP}{\code{I}}   % formal type parameter
\mynewcommand{\JP}{\code{J}}   % formal type parameter (for soundness proofs)


\mynewcommand{\Iparam}{Immutability parameter}
\mynewcommand{\iparam}{immutability parameter}
\mynewcommand{\iparams}{immutability parameters}
\mynewcommand{\Iparams}{Immutability parameters}
\mynewcommand{\Iarg}{Immutability argument}
\mynewcommand{\iarg}{immutability argument}
\mynewcommand{\iargs}{immutability arguments}
\mynewcommand{\Iargs}{Immutability arguments}
\mynewcommand{\ReadOnly}{\code{ReadOnly}}
\mynewcommand{\WriteOnly}{\code{WriteOnly}}
\mynewcommand{\None}{\code{None}}
\mynewcommand{\Mutable}{\code{Mutable}}
\mynewcommand{\Immut}{\code{Immut}}
\mynewcommand{\Raw}{\code{Raw}}


\mynewcommand{\This}{\code{This}}
\mynewcommand{\World}{\code{World}}


% Our annotations
\mynewcommand{\OMutable}{\code{@OMutable}}
\mynewcommand{\OI}{\code{@OI}}


\mynewcommand{\InVariantAnnot}{\code{@InVariant}}


\newcommand{\func}[1]{\text{\textnormal{\textit{\codesmaller #1}}}}


\mynewcommand{\st}{\ensuremath{\mathrel{{\leq}}}} %{\mathop{\textrm{\tt <:}}}
\mynewcommand{\notst}{\mathrel{\st\hspace{-1.5ex}\rule[-.25em]{.4pt}{1em}~}}
\mynewcommand{\tl}{\ensuremath{\triangleleft}}
\mynewcommand{\gap}{~ ~ ~ ~ ~ ~}


\newcommand{\RULE}[1]{\textsc{\scriptsize{}#1}} %\RULEhape\scriptsize}


\mynewcommand{\DA}{\texttt{DA}}
\mynewcommand{\ok}{\texttt{OK}}
\mynewcommand{\OK}{\texttt{OK}}
\mynewcommand{\IN}{\texttt{IN}}
\mynewcommand{\subterm}{\func{subterm}}
\mynewcommand{\TP}{\func{TP}} % function that returns type parameters in a type
\mynewcommand{\CT}{\func{CT}} % class table
\mynewcommand{\mtype}{\func{mtype}}
\mynewcommand{\mbody}{\func{mbody}}
\mynewcommand{\mmodifier}{\func{mmodifier}}
\mynewcommand{\fmodifier}{\func{fmodifier}}
\mynewcommand{\fields}{\func{fields}}
\mynewcommand{\cooked}{\func{cooked}}


\mynewcommand{\bound}{\func{bound}_\Delta}
\mynewcommand{\substitute}{\func{substitute}}
\mynewcommand{\ftype}{\func{ftype}}
\mynewcommand{\mguard}{\func{mguard}}
\mynewcommand{\isTransitive}{\func{isTransitive}}
\DeclareMathOperator{\dom}{dom}


\newcommand{\async}[1]{\code{async~\lb}#1\rb}
\newcommand{\finish}[1]{\code{finish~\lb}#1\rb}
\mynewcommand{\hasync}{\code{async}}
\mynewcommand{\hfinish}{\code{finish}}
%\newcommand{\Ofn}[1]{\ensuremath{O(#1)}}
\mynewcommand{\nonescaping}{\code{nonescaping}}

\mynewcommand{\hR}{\code{R}}
\mynewcommand{\hreceiver}{\code{receiver}} % receiver for new
\mynewcommand{\hSW}{\code{SW}}
\mynewcommand{\hAW}{\code{AW}}
\mynewcommand{\hObject}{\code{Object}}

\mynewcommand{\hG}{\code{G}}
\mynewcommand{\hP}{\code{P}}
\mynewcommand{\hd}{\code{d}}
\mynewcommand{\hdef}{\code{def}}
\mynewcommand{\hvar}{\code{var}}

\mynewcommand{\hescaping}{\code{escaping}}
\mynewcommand{\hextends}{\code{extends}}


\mynewcommand\xth{\xX{th}}
\mynewcommand\xrd{\xX{rd}}
\mynewcommand\xnd{\xX{nd}}
\mynewcommand\xst{\xX{st}}
\mynewcommand\ith{$i$\xth}
\mynewcommand\jth{$j$\xth}


\mynewcommand{\myindent}{~~}


% Add line between figure and text
\makeatletter
\def\topfigrule{\kern3\p@ \hrule \kern -3.4\p@} % the \hrule is .4pt high
\def\botfigrule{\kern-3\p@ \hrule \kern 2.6\p@} % the \hrule is .4pt high
\def\dblfigrule{\kern3\p@ \hrule \kern -3.4\p@} % the \hrule is .4pt high
\makeatother

\setlength{\textfloatsep}{.75\textfloatsep}


% Remove line between figure and its caption.  (The line is prettier, and
% it also saves a couple column-inches.)
\makeatletter
%\@setflag \@caprule = \@false
\makeatother


% http://www.tex.ac.uk/cgi-bin/texfaq2html?label=bold-extras
\usepackage{bold-extra}


% Left and right curly braces in tt font
\newcommand{\ttlcb}{\texttt{\char "7B}}
\newcommand{\ttrcb}{\texttt{\char "7D}}
\newcommand{\lb}{\ttlcb}
\newcommand{\rb}{\ttrcb}


\setlength{\leftmargini}{.75\leftmargini}
\def\comment#1{\typeout#1}
